a:Id, l:IdLnk, tg:Id. rcv(l,tg) = locl(a)  Knd  False 

latex

Definitions	Id, t  T, IdLnk, x:A. B(x), Knd, rcv(l,tg), Prop, False, P  Q, locl(a), P  Q, Dec(P)
Lemmas	decidable false, rcv wf, IdLnk wf, Id wf